3.4 Probability RTS (PRTS) Module

3.4 Probability RTS (PRTS) Module

Design and development of control software for safety-critical systems are notoriously difficult problems. Real-life systems often depend on quantitative timing. Furthermore, they may be required to satisfy requirements in an unreliable environment (e.g., unexpected user behaviors, communication failure). The combination of real-time and probability in complex hierarchical systems presents a unique challenge to system verification. Existing model checkers all have their limitation in this kind of system: UPPAAL is useful in real-time verification but does not support probabilistic choices; PRISM and MRMC lack real-time features although they could handle probabilistic models.

Since PAT could support real-time system models and PCSP models, we combine these two together to generate a new module that supports both timed features and probabilistic characteristics which is named as PRTS. This module inherits almost all the syntax and semantics from RTS and PCSP; what is more, it could verify all kinds of properties of those two moduls such as LTL checking, refinement checking, and deadlock checking.

PRTS could verify probabilistic, real-time, hierarchical systems, and its powerful expresiveness guarantees that many real-life systems could be handled by PAT in compact models. What is more, similar to RTS module, zone abstraction is used in PRTS to make sure that all the models could be transferred to finite-state Markov Decision Processes so that they are model checkable with our probabilistic algorithms. Considering the complex structure of this module, we are now developing it. So any feedback is warmly welcome.